Nuprl Lemma : alle-between1-not-first-since 11,40
es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} , p:({e:E| loc(e) = loc(e1)  Id} ).
e[e1,e2).e = first e  e1.p(e)  e[e1,e2).p(e) 
latex

Definitionsx:A. B(x), , P  Q, e[e1,e2).P(e), x(s), P & Q, P  Q, P  Q, t  T, x. t(x), A, e2 = first e  e1.P(e), (e <loc e'), WellFnd{i}(A;x,y.R(x;y)), {T}, False, Trans(T;x,y.E(x;y))
Lemmasalle-between1 wf, not wf, es-first-since wf, Id wf, es-loc wf, es-locl-wellfnd, es-le-loc, es-loc-pred, es-locl-iff, es-locl wf, es-le wf, es-locl-trans

origin